es-independent(es;i;k;x)
== s1, s2:(x:Idvartype(i;x)).
== s1  s2 mod x@i
==  (v:kindtype(i;k).
==  (Trans(i)(k,v,s1)  Trans(i)(k,v,s2) mod x@i & Send(i)(k,v,s1) = Send(i)(k,v,s2))
==  & (islocal(k)  Choose(i)(act(k),s1) = Choose(i)(act(k),s2)) 

latex

---

clarification:

es-independent(es;i;k;x)
== s1:(x:Ides-vartype(es; i; x)), s2:(x:Ides-vartype(es; i; x)).
== es-x-equiv(es;i;x;s1;s2)
==  (v:es-kindtype(es;i;k).
==  (es-x-equiv(es;i;x;es-trans(es;i)(k,v,s1);es-trans(es;i)(k,v,s2))
==  (& es-send(es;i)(k,v,s1) = es-send(es;i)(k,v,s2)  es-Msg(es) List)
==  & (islocal(k)
==  & ( es-choose(es;i)(act(k),s1)
==  & ( =
==  & ( es-choose(es;i)(act(k),s2)
==  & (  es-kindtype(es;i;k)+Unit) 

latex

Definitions	x:AB(x), Id, vartype(i;x), x:A. B(x), P & Q, s1  s2 mod x@i, Trans(i), type List, Msg, Send(i), P  Q, b, islocal(k), s = t, left+right, kindtype(i;k), Unit, f(a), Choose(i), act(k)
FDL editor aliases	es-independent